/**
 * 
 */
package extensionTools.smvCreator;

import java.util.ArrayList;

import extensionTools.smvCreator.Exceptions.RulesUtilsException;

/**
 * @author dani
 *
 */
public class ProcRule extends Rule {

        private String rules;
        /**
         * @param db
         */
        public ProcRule(DiagramDatabase db) {
                super(db);
                rules = "";
        }

        /* (non-Javadoc)
         * @see extensionTools.smvCreator.Rule#createRule()
         */
        /**
         * This function creates the case for processes in the system
         * @throws RulesUtilsException - when error occurred trying to convert an array
         */
        @Override
        public String createRule() throws RulesUtilsException {
                        for (SmvProcess proc : db.getSmvProcessList()) {
                        String procRule = "";
                for (int i=0; i < SMVCreator.K; i++)
                {
                        String procName = proc.getName()+"_"+i; 
                        
                        ArrayList<String> ruleForTermEv = new ArrayList<String>();
                        ruleForTermEv.add(SmvOp.createCaseLine(SmvOp.and(procName + "= active", SmvOp.and("sysState = step1","ev_terminate_"+procName + " = 0")),"notActive"));
                        ruleForTermEv.add(SmvOp.createCaseLine(SmvOp.and(procName + "= notActive", SmvOp.and("sysState = step2","ev_wait_"+procName + " = TRUE")),"waiting"));
                        ruleForTermEv.add(SmvOp.createCaseLine(SmvOp.and(procName + "= waiting", SmvOp.and("sysState = step2","ev_activate_"+procName + " = TRUE")),"active"));
                        ruleForTermEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = step2","ev_halt_"+procName + " = TRUE"),"notActive"));
                        ruleForTermEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = step1","ev_halt_"+procName + " = TRUE"),"notActive"));
                        ruleForTermEv.add(SmvOp.createCaseLine("TRUE" , procName));
                        
                        procRule = SmvOp.createCase(RulesUtils.arrayListToArray(ruleForTermEv));
                        procRule = SmvOp.next(procName, procRule);
                        rules += "\n" + procRule;       
                }
            }
            return rules;
        }

}
